Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT

摘要

In this paper we present the Transalg system, designed to produce SATencodings for discrete functions, written as programs in a specific language.Translation of such programs to SAT is based on propositional encoding methodsfor formal computing models and on the concept of symbolic execution. We usedthe Transalg system to make SAT encodings for a number of cryptographicfunctions.